\begin{tabbing}
effect{-}p(${\it es}$;$i$;${\it ds}$;$k$;$T$;$x$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$x$:Id. es{-}vartype(${\it es}$; $i$; $x$) $\subseteq\rho$ fpf{-}cap(${\it ds}$;IdDeq;$x$;Top)) \& es{-}kindtype(${\it es}$;$i$;$k$) $\subseteq\rho$ $T$\+
\\[0ex]\& alle{-}at(${\it es}$;$i$;$e$.\=es{-}kind(${\it es}$; $e$) $=$ $k$ $\in$ Knd\+
\\[0ex]$\Rightarrow$ \=es{-}valtype(${\it es}$; $e$) $\subseteq\rho$ $T$\+
\\[0ex]\& \=es{-}after(${\it es}$; $x$; $e$)\+
\\[0ex]$=$
\\[0ex]$f$(es{-}state{-}when(${\it es}$;$e$),es{-}val(${\it es}$; $e$))
\\[0ex]$\in$ fpf{-}cap(${\it ds}$;IdDeq;$x$;Top))
\-\-\-\-
\end{tabbing}